m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n))) 

latex

Definitions	S  T, Top, as @ bs, map(f;as), Unit, P  Q, i=j, , b, b, SQType(T), {T}, Prop, upto(n), i  j < k, P & Q, Dec(P), P  Q, AB, A, False, ij, P  Q, , {i..j}, x:A. B(x), t  T
Lemmas	int seg wf, nat wf, nat properties, ge wf, int sq, decidable int equal, le wf, upto wf, append nil sq, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, top wf, map wf, append assoc sq, map append sq